'''
Created on 2011-04-09

@author: kacper
'''
from dataStructs.definitions import Var, RelFac, Const, NotFormula, AndFormula,\
    OrFormula, ThenFormula, Default, Eq
from copy import deepcopy


tokens = (
    'PRO','AND','OR',
    'THEN','NOT','DEF',
    'LPAREN','RPAREN',
    'VAR' , 'CONST', 'COMMA', "NEWLINE", "EQ"
    )

# Tokens
t_PRO     = r':-'
t_AND     = r'&&'
t_OR      = r'\|\|'
t_THEN    = r'-\>'
t_NOT     = r'~'
t_DEF    =  r'=\>'
t_LPAREN  = r'\('
t_RPAREN  = r'\)'
t_VAR     = r'[A-Z][a-zA-Z0-9_]*'
t_CONST   = r'[a-z][a-zA-Z0-9_]*'
t_COMMA   = r','
t_EQ      = r'='


# Ignored characters
t_ignore = " \t"

def t_newline(t):
    r'\n+'
    t.lexer.lineno += t.value.count("\n")
    
def t_error(t):
    print("Illegal character '%s'" % t.value[0])
    t.lexer.skip(1)
    
# Build the lexer
import ply.lex as lex
lex.lex()


# Parsing rules

precedence = (
    ('left','PRO'),
    ('left','THEN'),
    ('left','OR'),
    ('left','AND'),
    ('right','UNOT'),
    )


def p_prog(t):
    '''prog : statement prog'''
    t[2].append(t[1])
    t[0] = t[2]
    
def p_emp_prog(t): 
    '''prog :  empty'''
    t[0] = []

def p_empty(p):
    'empty :'
    pass


def p_statement_assign(t):
    'statement : formula'
    t[0] = t[1]


def p_statement_expr(t):
    'statement : formula DEF formula'
    t[0] = Default(t[1],t[3])

def p_statement_pro(t):
    'statement : formula PRO formula'
    t[0] = ThenFormula(t[3],t[1])

def p_expression_binop(t):
    '''formula : formula AND formula 
        | formula OR formula 
        |  formula THEN  formula'''
    if t[2] == "&&"  : t[0] = AndFormula(t[1],t[3])
    elif t[2] == "||": t[0] = OrFormula(t[1],t[3])
    elif t[2] == "->": t[0] = ThenFormula(t[1],t[3])
    

def p_expression_uminus(t):
    'formula : NOT formula %prec UNOT'
    t[0] = NotFormula(t[2])

def p_expression_group(t):
    'formula : LPAREN formula RPAREN'
    t[0] = t[2]


def p_var(t):
    'formula : VAR'
    t[0] = Var(t[1])

def p_const(t):
    'formula : CONST'
    t[0] = Const(t[1])

def p_relation(t):
    'formula : relation'
    t[0] = t[1]
    
    

def p_relation_arg(t):
    'relation : CONST LPAREN listargs  RPAREN '
    j = deepcopy( t[3][0])
    j.reverse()
    #print j
    cls = RelFac(t[1],(),{"nargs":t[3][1], "th_id":theory_id})
    t[0] = cls(j)
    #print t[0]

def p_list_args_end(t):
    'listargs : term'
    t[0] =[[t[1]],0] 
    
def p_list_args_more(t): 
    'listargs : term COMMA listargs'
    t[3][0].append(t[1])
    t[3][1] += 1
    t[0] = t[3] 

def p_term_args(t):
    'term : VAR'
    t[0] = Var(t[1])

def p_term_rel(t):
    'term : CONST '
    t[0] = Const(t[1]) 


def p_error(t):
    print("Syntax error at '%s'" % t.value)
    raise SyntaxError("Syntax error at '%s'" % str(t))

import ply.yacc as yacc
parser = yacc.yacc()

theory_id =0 
#'''
#def sents_parse( fileName ):
#    f= open(fileName)
#    program = [ parser.parse(x) for x in f.readlines() ]
#    return program
#'''
def sents_parse( fileName, theory =0 ):
    f= open(fileName)
    theory_id = theory
    program = [ parser.parse(x) for x in f.readlines() ]
    program = sum( program,[])
    return program

def sents_parse_string(formula, theory =0):
    theory_id = theory
    #print "fucking formula", formula
    program = parser.parse(formula)
    #print "fucking formula", program
    return program


#
#while 1:
#    try:
#        s = open('try.lg')   # Use raw_input on Python 2
#    except EOFError:
#        break
#    yacc.parse(s)